E, X1, X2:Type, info:(E(IdX1+(IdLnkE)X2)), e:E. rcv?(e)  sender(e)  E 

latex

Definitions	rcv?(e), sender(e), ecase1(e;info;i.f(i);l,e'.g(l;e')), x:A. B(x), Id, IdLnk, b, False, P  Q, t  T, True
Lemmas	true wf, false wf, IdLnk wf, Id wf, rcv? wf, assert wf